Section: New Results

Formal proof in real algebraic geometry

Participants : Assia Mahboubi [Contact] , Cyril Cohen.

Cyril Cohen and Assia Mahboubi have completed the first formal proof of quantifier elimination for the theory of real closed fields. This work includes a significant part of infrastructure code for ordered algebraic theories, intervals, and polynomials. This work is described in a submitted paper [29] .

Cyril Cohen has implemented in Coq a construction of real algebraic numbers and proved it had a structure of discrete Archimedian real closed field, in the sense of the previous proof of quantifier elimination. Beside the computational interest of real algebraic numbers, this construction both legitimates the abstraction chosen for the proof of quantifier elimination and provides a basis for complex algebraic numbers needed for the completion of the formal proof of the Feit-Thompson theorem. This work is described in a paper to appear in the proceedings of the JFLA2011 conference.